A, B:(IdMsgA).
A || B  interface-compatible(A;B)  Feasible(A)  Feasible(B)  Feasible(A  B) 

latex

Definitions

, t  T, M(i), P & Q, A  B, Feasible(D), A || B, P  Q, x:A. B(x), interface-link(A;B;l;tg), P  Q, P  Q, x. t(x), x(s), ff, tt, i <z j, b, tl(l), i z j, if b then t else f fi , nth_tl(n;as), hd(l), Y, False, A, A  B, l[i], ||as||, A c B, , (x  l), x:A. B(x), (xL.P(x)), interface-compatible(A;B), b, P  Q

Lemmas

msga wf, ma-compat wf, interface-compatible wf, ma-sends-on wf, assert wf, finite-type wf, ldst wf, ma-din wf, lsrc wf, ma-dout wf, ma-feasible wf, IdLnk wf, Id wf, ma-join-feasible, l all nil, and functionality wrt iff, l all cons, decidable wf, l all wf, iff transitivity, decidable assert, decidable equal Id, decidable cand, ma-join wf, finite-set-type-cases, l member wf, select wf, le wf, ma-join-sends-on